<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>Grammar</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="Grammar";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/EarleyParser.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/GrammarAmbiguity.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/Grammar.html" target="_top">Frames</a></li>
<li><a href="Grammar.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.verify</div>
<h2 title="Class Grammar" class="title">Class Grammar</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.verify.Grammar</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">Grammar</span>
extends java.lang.Object
implements <a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></pre>
<div class="block">Grammar processes a mmj LogicalSystem, extracts a Grammar, which it also
 validates, and parses statements in the system.
 <p>
 The first thing to note is that Grammar builds a "grammar" -- a set of
 replacement rules -- from a Metamath ".mm" file/database. The distinction
 made between "building" and extracting what is already there is important
 because Metamath's set.mm database uses "overloaded functions", such as "weq"
 and "wceq", which are tecnically "ambiguous" (two valid parse trees exist.)
 <p>
 These "non-essential" ambiguities are resolved during grammar generation by a
 process of "combinatorial explosion", which creates a Notation Rule for every
 permutation of input parameters, and then priorities those rules -- first
 come, first served, dropping any duplicates. Assuming that "weq" precedes
 "wceq" in the database, "set = set" will always parse to "weq" and the other
 variations such as "set = class", "class = set" will parse to "wceq".
 <p>
 The second important topic is that Grammar imposes new validation rules on a
 Metamath .mm file/database. But these rules never come into force unless a
 user desires to use Grammar to perform parsing (aka "syntactical analysis".)
 A user with a non-Grammar compliant database can still use mmj to perform
 Proof Verification and to print reports.
 <p>
 The additional mmj validation rules are not extremely restrictive, and in
 fact, the entire mmj system is designed to operate on set.mm with no changes
 to any default parameters or settings. Let me give examples.
 <p>
 The Metamath symbol "|-" termed "It is provable that..." is the default in
 mmj, and it is given a special name, the "provableLogicStmtTyp". If your .mm
 file uses a different symbol, you must tell mmj (via mmj.util.RunParmFile or
 a constructor parameter.) Moreover, if your .mm file encodes a new logical
 theory involving TWO provableLogicStmtTyp codes, you're going to be hit with
 an error, and Grammar will refuse to continue. In addition, your
 provableLogicStmtTyp code cannot be the Type Code of any variables in your
 system -- you cannot define a Syntax Axiom for it, and you thus, cannot do a
 Meta-Metamath theory using that approach (not directly anyway.) There may be
 an important need for two provableLogicStmtTyp codes in a single .mm file,
 but my imagination is limited, and so was my time. Another restriction is
 using a grammatical Type Code as a constant in an expression, for example,
 like this: "xyz $p |- ( wff -> ph ) $.", where "wff" is a Type Code for
 "well-formed formula" variables. See
 ConsolidatedListOfGrammarValidations.html for more info.
 <p>
 One excuse I must make is that the Grammar Rule Trees and Forests
 (mmj.verify.GRForest.java and mmj.verify.GRNode.java) were part of the
 BottomUpParser.java debacle. They are still used for detecting duplicate
 NotationRules and for printing out the rules, but if I were starting from
 scratch I would not use them.
 <p>
 Finally, mmj.verify.GrammarAmbiguity.java is mostly a stub -- incomplete.
 There is a lot of work needed to detect and report on grammatical
 ambiguities, we've just scratched the surface. In fact, according to a famous
 parsing techniques expert, developing a generalized program able to process
 any context-free grammar and decide whether it is unambiguous is
 mathematically impossible. So that is definitely an opportunity for
 achievement, right there. It will take a bit longer than initially expected
 :)</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../ConsolidatedListOfGrammarValidations.html">
      ConsolidatedListOfGrammarValidations.html</a>, 
<a href="../../BasicsOfSyntaxAxiomsAndTypes.html">
      BasicsOfSyntaxAxiomsAndTypes.html</a>, 
<a href="../../EssentialAmbiguityExamples.html">
      EssentialAmbiguityExamples.html</a>, 
<a href="../../CreatingGrammarRulesFromSyntaxAxioms.html">
      CreatingGrammarRulesFromSyntaxAxioms.html</a>, 
<a href="../../GrammarRuleTreeNotes.html"> GrammarRuleTreeNotes.html</a>, 
<a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/Grammar.html#Grammar()">Grammar</a></strong>()</code>
<div class="block">Constructor using all default values for doCompleteStmtAmbiguityEdits,
 doCompleteGrammarAmbiguityEdits, provableLogicStmtTyp Code (ie "|-") and
 logicStmtTyp Code (ie "wff").</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/Grammar.html#Grammar(java.lang.String[], java.lang.String[])">Grammar</a></strong>(java.lang.String[]&nbsp;provableLogicStmtTypCodes,
       java.lang.String[]&nbsp;logicStmtTypCodes)</code>
<div class="block">Constructor using default doCompleteStmtAmbiguityEdits and
 doCompleteGrammarAmbiguityEdits values.</div>
</td>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/Grammar.html#Grammar(java.lang.String[], java.lang.String[], boolean)">Grammar</a></strong>(java.lang.String[]&nbsp;provableLogicStmtTypCodes,
       java.lang.String[]&nbsp;logicStmtTypCodes,
       boolean&nbsp;doCompleteGrammarAmbiguityEdits)</code>
<div class="block">Constructor using default doCompleteStmtAmbiguityEdits value.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colOne"><code><strong><a href="../../mmj/verify/Grammar.html#Grammar(java.lang.String[], java.lang.String[], boolean, boolean)">Grammar</a></strong>(java.lang.String[]&nbsp;provableLogicStmtTypCodes,
       java.lang.String[]&nbsp;logicStmtTypCodes,
       boolean&nbsp;doCompleteGrammarAmbiguityEdits,
       boolean&nbsp;doCompleteStmtAmbiguityEdits)</code>
<div class="block">Constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#assignNextGrammarRuleNbr()">assignNextGrammarRuleNbr</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#derivedRuleQueueAdd(mmj.verify.GrammarRule)">derivedRuleQueueAdd</a></strong>(<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a>&nbsp;gR)</code>
<div class="block">Add rule to derivedRuleQueue.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#derivedRuleQueueInit()">derivedRuleQueueInit</a></strong>()</code>
<div class="block">Initialize derivedRuleQueue.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#derivedRuleQueueRead()">derivedRuleQueueRead</a></strong>()</code>
<div class="block">Read GrammarRule from derivedRuleQueue.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getGrammarInitialized()">getGrammarInitialized</a></strong>()</code>
<div class="block">Return grammarInitialized flag.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getLogicStmtTypArray()">getLogicStmtTypArray</a></strong>()</code>
<div class="block">Return Array of Logic Stmt Type Codes (like "wff").</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getNotationGRGimmeMatchCnt()">getNotationGRGimmeMatchCnt</a></strong>()</code>
<div class="block">Get Count of NotationRules deemed to be "gimme matches".</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.Set&lt;<a href="../../mmj/verify/NotationRule.html" title="class in mmj.verify">NotationRule</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getNotationGRSet()">getNotationGRSet</a></strong>()</code>
<div class="block">Return NotationRule Set.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getNullsPermittedGRList()">getNullsPermittedGRList</a></strong>()</code>
<div class="block">Return NullsPermittedRule List.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.Set&lt;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getNullsPermittedTypSet()">getNullsPermittedTypSet</a></strong>()</code>
<div class="block">Return NullsPermittedRule Type Code Set.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getProvableLogicStmtTypArray()">getProvableLogicStmtTypArray</a></strong>()</code>
<div class="block">Return Array of Provable Logic Stmt Type Codes (like "|-").</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getSymTblSize()">getSymTblSize</a></strong>()</code>
<div class="block">Return size of Symbol Table.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.Set&lt;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getSyntaxAxiomTypSet()">getSyntaxAxiomTypSet</a></strong>()</code>
<div class="block">Return Syntax Axiom Type Code Set.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getTypeConversionGRList()">getTypeConversionGRList</a></strong>()</code>
<div class="block">Return TypeConversionRule List.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.Set&lt;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#getVarHypTypSet()">getVarHypTypSet</a></strong>()</code>
<div class="block">Return VarHyp Type Code Set.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#incNotationGRGimmeMatchCnt()">incNotationGRGimmeMatchCnt</a></strong>()</code>
<div class="block">Increment (add 1) to Count to NotationRules deemed to be "gimme matches".</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#initializeGrammar(mmj.lang.Messages, java.util.Map, java.util.Map)">initializeGrammar</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                 java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTblParam,
                 java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTblParam)</code>
<div class="block">Initializes the grammar.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#notationGRSetAdd(mmj.verify.NotationRule)">notationGRSetAdd</a></strong>(<a href="../../mmj/verify/NotationRule.html" title="class in mmj.verify">NotationRule</a>&nbsp;notationRule)</code>
<div class="block">Add NotationRule to Notation Rule Set.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#nullsPermittedGRListAdd(mmj.verify.NullsPermittedRule)">nullsPermittedGRListAdd</a></strong>(<a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&nbsp;r)</code>
<div class="block">Add NullsPermittedRule to List.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#parseAllFormulas(mmj.lang.Messages, java.util.Map, java.util.Map)">parseAllFormulas</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTblParam,
                java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTblParam)</code>
<div class="block">Parse all Statement Formulas and update stmtTbl with results.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#parseFormula(mmj.lang.Messages, java.util.Map, java.util.Map, mmj.lang.Formula, mmj.lang.VarHyp[], int, mmj.lang.Stmt)">parseFormula</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
            java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
            java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
            <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;formula,
            <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray,
            int&nbsp;highestSeq,
            <a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;defaultStmt)</code>
<div class="block">Parse a single formula.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#parseFormulaWithoutSafetyNet(mmj.lang.Formula, mmj.lang.Hyp[], int)">parseFormulaWithoutSafetyNet</a></strong>(<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;formula,
                            <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;hypArray,
                            int&nbsp;highestSeq)</code>
<div class="block">Alternate access to parse algorithm for use in Proof Assistant with no
 pre-check of Grammar initialization or error messages.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#parseOneStmt(mmj.lang.Messages, java.util.Map, java.util.Map, mmj.lang.Stmt)">parseOneStmt</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
            java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
            java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
            <a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;stmt)</code>
<div class="block">Parse a single Statement.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#setDerivedRuleQueue(java.util.PriorityQueue)">setDerivedRuleQueue</a></strong>(java.util.PriorityQueue&lt;<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a>&gt;&nbsp;p)</code>
<div class="block">Set derivedRuleQueue.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#setGrammarInitializedFalse()">setGrammarInitializedFalse</a></strong>()</code>
<div class="block">Set grammarInitialized flag to false.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#setNotationGRGimmeMatchCnt(int)">setNotationGRGimmeMatchCnt</a></strong>(int&nbsp;cnt)</code>
<div class="block">Set Count of NotationRules deemed to be "gimme matches".</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/verify/Grammar.html#typeConversionGRListAdd(mmj.verify.TypeConversionRule)">typeConversionGRListAdd</a></strong>(<a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;typeConversionRule)</code>
<div class="block">Add TypeConversionRule to List.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="Grammar(java.lang.String[], java.lang.String[], boolean, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Grammar</h4>
<pre>public&nbsp;Grammar(java.lang.String[]&nbsp;provableLogicStmtTypCodes,
       java.lang.String[]&nbsp;logicStmtTypCodes,
       boolean&nbsp;doCompleteGrammarAmbiguityEdits,
       boolean&nbsp;doCompleteStmtAmbiguityEdits)</pre>
<div class="block">Constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>provableLogicStmtTypCodes</code> - lists Type Codes used on Theorems
            involving Logical Statements thus identifying all other Type
            Codes as Syntax Type Codes -- if array is empty or null, the
            default is "|-".</dd><dd><code>logicStmtTypCodes</code> - - lists Type Codes used on statements of logic
            (such as "wff" but not "set", etc) -- if array is empty or
            null, the default is "wff".</dd><dd><code>doCompleteGrammarAmbiguityEdits</code> - Thorough (attempt to) prove
            grammar is not Ambiguous. If Ambiguity is found, an error
            message is generated (hopefully listing a formula with two
            different grammatical parsings in RPN format.) These edits are
            redundant unless the grammar or software have changed since
            the last edit; and they may be long and tedious, which is why
            this option is provided. The default is True.</dd><dd><code>doCompleteStmtAmbiguityEdits</code> - Check each non-Grammar Stmt being
            parsed to see if there are two different, valid parse trees --
            meaning that the Stmt is ambiguous, an error. Note that this
            option will often require much more time due to generation of
            many duplicate parse trees (not an error).</dd></dl>
</li>
</ul>
<a name="Grammar(java.lang.String[], java.lang.String[], boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Grammar</h4>
<pre>public&nbsp;Grammar(java.lang.String[]&nbsp;provableLogicStmtTypCodes,
       java.lang.String[]&nbsp;logicStmtTypCodes,
       boolean&nbsp;doCompleteGrammarAmbiguityEdits)</pre>
<div class="block">Constructor using default doCompleteStmtAmbiguityEdits value.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>provableLogicStmtTypCodes</code> - lists Type Codes used on Theorems
            involving Logical Statements thus identifying all other Type
            Codes as Syntax Type Codes -- if array is empty or null, the
            default is "|-".</dd><dd><code>logicStmtTypCodes</code> - - lists Type Codes used on statements of logic
            (such as "wff" but not "set", etc) -- if array is empty or
            null, the default is "wff".</dd><dd><code>doCompleteGrammarAmbiguityEdits</code> - Thorough (attempt to) prove
            grammar is not Ambiguous. If Ambiguity is found, an error
            message is generated (hopefully listing a formula with two
            different grammatical parsings in RPN format.) These edits are
            redundant unless the grammar or software have changed since
            the last edit; and they may be long and tedious, which is why
            this option is provided. The default is True.</dd></dl>
</li>
</ul>
<a name="Grammar(java.lang.String[], java.lang.String[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Grammar</h4>
<pre>public&nbsp;Grammar(java.lang.String[]&nbsp;provableLogicStmtTypCodes,
       java.lang.String[]&nbsp;logicStmtTypCodes)</pre>
<div class="block">Constructor using default doCompleteStmtAmbiguityEdits and
 doCompleteGrammarAmbiguityEdits values.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>provableLogicStmtTypCodes</code> - lists Type Codes used on Theorems
            involving Logical Statements thus identifying all other Type
            Codes as Syntax Type Codes -- if array is empty or null, the
            default is "|-".</dd><dd><code>logicStmtTypCodes</code> - - lists Type Codes used on statements of logic
            (such as "wff" but not "set", etc) -- if array is empty or
            null, the default is "wff".</dd></dl>
</li>
</ul>
<a name="Grammar()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>Grammar</h4>
<pre>public&nbsp;Grammar()</pre>
<div class="block">Constructor using all default values for doCompleteStmtAmbiguityEdits,
 doCompleteGrammarAmbiguityEdits, provableLogicStmtTyp Code (ie "|-") and
 logicStmtTyp Code (ie "wff").</div>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="assignNextGrammarRuleNbr()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>assignNextGrammarRuleNbr</h4>
<pre>public&nbsp;int&nbsp;assignNextGrammarRuleNbr()</pre>
</li>
</ul>
<a name="getGrammarInitialized()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getGrammarInitialized</h4>
<pre>public&nbsp;boolean&nbsp;getGrammarInitialized()</pre>
<div class="block">Return grammarInitialized flag.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>grammarInitialized flag.</dd></dl>
</li>
</ul>
<a name="setGrammarInitializedFalse()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setGrammarInitializedFalse</h4>
<pre>public&nbsp;void&nbsp;setGrammarInitializedFalse()</pre>
<div class="block">Set grammarInitialized flag to false. (Don't allow it to be set to true
 externally.)</div>
</li>
</ul>
<a name="derivedRuleQueueInit()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>derivedRuleQueueInit</h4>
<pre>public&nbsp;void&nbsp;derivedRuleQueueInit()</pre>
<div class="block">Initialize derivedRuleQueue.</div>
</li>
</ul>
<a name="setDerivedRuleQueue(java.util.PriorityQueue)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setDerivedRuleQueue</h4>
<pre>public&nbsp;void&nbsp;setDerivedRuleQueue(java.util.PriorityQueue&lt;<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a>&gt;&nbsp;p)</pre>
<div class="block">Set derivedRuleQueue.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>p</code> - PriorityQueue.</dd></dl>
</li>
</ul>
<a name="derivedRuleQueueAdd(mmj.verify.GrammarRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>derivedRuleQueueAdd</h4>
<pre>public&nbsp;void&nbsp;derivedRuleQueueAdd(<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a>&nbsp;gR)</pre>
<div class="block">Add rule to derivedRuleQueue.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>gR</code> - GrammarRule to add.</dd></dl>
</li>
</ul>
<a name="derivedRuleQueueRead()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>derivedRuleQueueRead</h4>
<pre>public&nbsp;<a href="../../mmj/verify/GrammarRule.html" title="class in mmj.verify">GrammarRule</a>&nbsp;derivedRuleQueueRead()</pre>
<div class="block">Read GrammarRule from derivedRuleQueue.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>GrammarRule, or null if queue empty.</dd></dl>
</li>
</ul>
<a name="getSymTblSize()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSymTblSize</h4>
<pre>public&nbsp;int&nbsp;getSymTblSize()</pre>
<div class="block">Return size of Symbol Table.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>size of Symbol Table.</dd></dl>
</li>
</ul>
<a name="notationGRSetAdd(mmj.verify.NotationRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>notationGRSetAdd</h4>
<pre>public&nbsp;void&nbsp;notationGRSetAdd(<a href="../../mmj/verify/NotationRule.html" title="class in mmj.verify">NotationRule</a>&nbsp;notationRule)</pre>
<div class="block">Add NotationRule to Notation Rule Set.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>notationRule</code> - to add to set.</dd></dl>
</li>
</ul>
<a name="getNotationGRSet()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getNotationGRSet</h4>
<pre>public&nbsp;java.util.Set&lt;<a href="../../mmj/verify/NotationRule.html" title="class in mmj.verify">NotationRule</a>&gt;&nbsp;getNotationGRSet()</pre>
<div class="block">Return NotationRule Set.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Set of NotationRules.</dd></dl>
</li>
</ul>
<a name="incNotationGRGimmeMatchCnt()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>incNotationGRGimmeMatchCnt</h4>
<pre>public&nbsp;void&nbsp;incNotationGRGimmeMatchCnt()</pre>
<div class="block">Increment (add 1) to Count to NotationRules deemed to be "gimme matches".</div>
</li>
</ul>
<a name="setNotationGRGimmeMatchCnt(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setNotationGRGimmeMatchCnt</h4>
<pre>public&nbsp;void&nbsp;setNotationGRGimmeMatchCnt(int&nbsp;cnt)</pre>
<div class="block">Set Count of NotationRules deemed to be "gimme matches".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>cnt</code> - Count of NotationRules deemed to be "gimme matches".</dd></dl>
</li>
</ul>
<a name="getNotationGRGimmeMatchCnt()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getNotationGRGimmeMatchCnt</h4>
<pre>public&nbsp;int&nbsp;getNotationGRGimmeMatchCnt()</pre>
<div class="block">Get Count of NotationRules deemed to be "gimme matches".</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Count of NotationRules deemed to be "gimme matches".</dd></dl>
</li>
</ul>
<a name="typeConversionGRListAdd(mmj.verify.TypeConversionRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>typeConversionGRListAdd</h4>
<pre>public&nbsp;int&nbsp;typeConversionGRListAdd(<a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&nbsp;typeConversionRule)</pre>
<div class="block">Add TypeConversionRule to List.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typeConversionRule</code> - to be added.</dd>
<dt><span class="strong">Returns:</span></dt><dd>index of new rule in list.</dd></dl>
</li>
</ul>
<a name="getTypeConversionGRList()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTypeConversionGRList</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/verify/TypeConversionRule.html" title="class in mmj.verify">TypeConversionRule</a>&gt;&nbsp;getTypeConversionGRList()</pre>
<div class="block">Return TypeConversionRule List.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>TypeConversionRule List.</dd></dl>
</li>
</ul>
<a name="nullsPermittedGRListAdd(mmj.verify.NullsPermittedRule)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>nullsPermittedGRListAdd</h4>
<pre>public&nbsp;int&nbsp;nullsPermittedGRListAdd(<a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&nbsp;r)</pre>
<div class="block">Add NullsPermittedRule to List.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>r</code> - NullsPermittedRule to be added.</dd>
<dt><span class="strong">Returns:</span></dt><dd>index of new NullsPermittedRule.</dd></dl>
</li>
</ul>
<a name="getNullsPermittedGRList()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getNullsPermittedGRList</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/verify/NullsPermittedRule.html" title="class in mmj.verify">NullsPermittedRule</a>&gt;&nbsp;getNullsPermittedGRList()</pre>
<div class="block">Return NullsPermittedRule List.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>NullsPermittedRule List.</dd></dl>
</li>
</ul>
<a name="getNullsPermittedTypSet()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getNullsPermittedTypSet</h4>
<pre>public&nbsp;java.util.Set&lt;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&gt;&nbsp;getNullsPermittedTypSet()</pre>
<div class="block">Return NullsPermittedRule Type Code Set.
 <p>
 This is the set of Type Codes for which Nulls are permitted.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>NullsPermittedRule Type Code Set.</dd></dl>
</li>
</ul>
<a name="getVarHypTypSet()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getVarHypTypSet</h4>
<pre>public&nbsp;java.util.Set&lt;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&gt;&nbsp;getVarHypTypSet()</pre>
<div class="block">Return VarHyp Type Code Set. This is the set of Type Codes with defined
 VarHyp's.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>VarHyp Type Code Set.</dd></dl>
</li>
</ul>
<a name="getSyntaxAxiomTypSet()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSyntaxAxiomTypSet</h4>
<pre>public&nbsp;java.util.Set&lt;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&gt;&nbsp;getSyntaxAxiomTypSet()</pre>
<div class="block">Return Syntax Axiom Type Code Set.
 <p>
 This is the set of Type Codes for Syntax Axioms are defined.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Syntax Axiom Type Code Set.</dd></dl>
</li>
</ul>
<a name="getLogicStmtTypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogicStmtTypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;getLogicStmtTypArray()</pre>
<div class="block">Return Array of Logic Stmt Type Codes (like "wff").
 <p>
 At this time, the array will have exactly one element.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Array of Logic Stmt Type Codes.</dd></dl>
</li>
</ul>
<a name="getProvableLogicStmtTypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProvableLogicStmtTypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>[]&nbsp;getProvableLogicStmtTypArray()</pre>
<div class="block">Return Array of Provable Logic Stmt Type Codes (like "|-"). At this time,
 the array will have exactly one element.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Array of Logic Stmt Type Codes.</dd></dl>
</li>
</ul>
<a name="parseOneStmt(mmj.lang.Messages, java.util.Map, java.util.Map, mmj.lang.Stmt)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>parseOneStmt</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;parseOneStmt(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
                     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
                     <a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;stmt)</pre>
<div class="block">Parse a single Statement.
 <p>
 If used with VarHyp or SyntaxAxiom, simply returns
 stmt.getExprParseTree().
 <p>
 Note: access to symTbl and stmtTbl is required in case the grammar needs
 to be re-initialized.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SyntaxVerifier.html#parseOneStmt(mmj.lang.Messages, java.util.Map, java.util.Map, mmj.lang.Stmt)">parseOneStmt</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for error/info messages.</dd><dd><code>symTbl</code> - Symbol Table (Map).</dd><dd><code>stmtTbl</code> - Statement Table (Map).</dd><dd><code>stmt</code> - Stmt in stmtTbl to parse.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ParseTree of Stmt</dd></dl>
</li>
</ul>
<a name="parseFormula(mmj.lang.Messages, java.util.Map, java.util.Map, mmj.lang.Formula, mmj.lang.VarHyp[], int, mmj.lang.Stmt)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>parseFormula</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;parseFormula(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
                     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
                     <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;formula,
                     <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray,
                     int&nbsp;highestSeq,
                     <a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;defaultStmt)</pre>
<div class="block">Parse a single formula.
 <p>
 Note: access to symTbl and stmtTbl is required in case the grammar needs
 to be re-initialized.
 <p>
 Note: <b>highestSeq</b> is similar to the restriction in proof
 verification: a proof can only refer to previous statements. However,
 setting this to java.lang.Integer.MAX_VALUE says, parse this formula with
 the entire grammar -- which ought to result in the same parse, unless the
 grammar is ambiguous (new Grammar Rules should be "disjoint" from
 previous ones.)</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SyntaxVerifier.html#parseFormula(mmj.lang.Messages, java.util.Map, java.util.Map, mmj.lang.Formula, mmj.lang.VarHyp[], int, mmj.lang.Stmt)">parseFormula</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for error/info messages.</dd><dd><code>symTbl</code> - Symbol Table (Map).</dd><dd><code>stmtTbl</code> - Statement Table (Map).</dd><dd><code>formula</code> - Formula to parse.</dd><dd><code>varHypArray</code> - VarHyp's for the Formula's Var's.</dd><dd><code>highestSeq</code> - Max MObj.seq that can be referenced.</dd><dd><code>defaultStmt</code> - Default Stmt for output RPN/message.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ParseTree of Stmt containing RPN.</dd></dl>
</li>
</ul>
<a name="parseAllFormulas(mmj.lang.Messages, java.util.Map, java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>parseAllFormulas</h4>
<pre>public&nbsp;void&nbsp;parseAllFormulas(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                    java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTblParam,
                    java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTblParam)</pre>
<div class="block">Parse all Statement Formulas and update stmtTbl with results.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SyntaxVerifier.html#parseAllFormulas(mmj.lang.Messages, java.util.Map, java.util.Map)">parseAllFormulas</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for error/info messages.</dd><dd><code>symTblParam</code> - Symbol Table (Map).</dd><dd><code>stmtTblParam</code> - Statement Table (Map).</dd></dl>
</li>
</ul>
<a name="initializeGrammar(mmj.lang.Messages, java.util.Map, java.util.Map)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>initializeGrammar</h4>
<pre>public&nbsp;boolean&nbsp;initializeGrammar(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                        java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTblParam,
                        java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTblParam)</pre>
<div class="block">Initializes the grammar.
 <p>
 Normally this is handled automatically. It initializes "the grammar" but
 does not parse every Stmt in stmtTbl.
 <p>
 The intended use of this function would be to initialize the grammar
 without parsing every statement (parsing every statement in set.mm
 requires 8ish seconds!)</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/SyntaxVerifier.html#initializeGrammar(mmj.lang.Messages, java.util.Map, java.util.Map)">initializeGrammar</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/lang/SyntaxVerifier.html" title="interface in mmj.lang">SyntaxVerifier</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for error/info messages.</dd><dd><code>symTblParam</code> - Symbol Table (Map).</dd><dd><code>stmtTblParam</code> - Statement Table (Map).</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if grammar initializes successfully, else false.</dd></dl>
</li>
</ul>
<a name="parseFormulaWithoutSafetyNet(mmj.lang.Formula, mmj.lang.Hyp[], int)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>parseFormulaWithoutSafetyNet</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;parseFormulaWithoutSafetyNet(<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;formula,
                                     <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>[]&nbsp;hypArray,
                                     int&nbsp;highestSeq)</pre>
<div class="block">Alternate access to parse algorithm for use in Proof Assistant with no
 pre-check of Grammar initialization or error messages.
 <p>
 This method assumes that we're being invoked from someplace like
 BatchMMJ2 that has already confirmed that the Grammar is initialized. In
 theory this could cause a problem if a non-syntax error comes out and is
 taken as a syntax error by the user. However, with the current parser
 that should not be a problem (as seen in the following method).</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>formula</code> - formula to be parsed.</dd><dd><code>hypArray</code> - Hyp's for Formula's Var's.</dd><dd><code>highestSeq</code> - Maximum Stmt.seq that may be used to parse the
            expression.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ParseTree or null if parse errors.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/verify/EarleyParser.html" title="class in mmj.verify"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/verify/GrammarAmbiguity.html" title="class in mmj.verify"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/verify/Grammar.html" target="_top">Frames</a></li>
<li><a href="Grammar.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
